es:event_system{i:l}, i:Id, L:(Knd List), x:Id, T:Type.
(es-isconst(es; i; x))  frame-p(es; i; T; x; L)  @i only L affect x:T 

latex

Definitions	A c B, @i only L affect x:T, x:A  B(x), frame-p(es; i; T; x; L), event_system{i:l}, t  T, Id, Knd, type List, Type, x:A. B(x), es-isconst(es; i; x), b, P  Q, es-vartype(es; i; x), P  Q, es-dtype(es; i; x; T), x:AB(x), es-kind(es; e), (x  l), A, s = t, loc(e), prop{i:l}, es-E(es), alle-at(es; i; e.P(e)), , #$n, es-when(es; x; e), es-after(es; x; e)
Lemmas	int inc rationals, es-E wf, es-loc wf, not wf, l member wf, es-kind wf, frame-p wf, assert wf, es-isconst wf, Knd wf, Id wf, event system wf